T:Type, f:(TT), L:(T List), x, y, a, b:T. x=f*(y) via L  a before b  L  a is f*(b) 

latex

Definitions

x:A. B(x), P  Q, y is f*(x), x before y  l, y=f*(x) via L, x:AB(x), Type, s = t, t  T, type List, hd(l), (x  l), L1  L2, x:A. B(x), {i..j}, -n, f(a), l[i], n+m, last(L), , [], False, Void, x:A  B(x), A, <a, b>, P & Q, A c B, , #$n, a < b, [car / cdr], A List, P  Q, ||as||, P  Q, left + right, {T}, P  Q, (xL.P(x)), xL. P(x), x f y, a < b, a <p b, a  b, a ~ b, b | a, b, Dec(P), , {x:A| B(x)} , Y, x.A(x), rec-case(a) of [] => s | x::y => z.t(x;y;z), nth_tl(n;as), if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), i z j, b, i <z j, if a<b then c else d, n - m, tl(l), i  j , A  B, , , Unit, |r|, |g|, |p|, x,y:A//B(x;y), Atom, SQType(T), s ~ t

Lemmas

hd wf, l before member, fun-connected transitivity, guard wf, cons member, false wf, decidable wf, fun-connected-step, length wf1, non neg length, l member wf, decidable lt, nil member, cons before, fun-path-cons, int seg wf, not wf, fun-path wf, l before wf, fun-connected wf